Eléments de l'association
|
List of bibliographic references
Number of relevant bibliographic references: 92.Ident. | Authors (with country if any) | Title |
---|---|---|
000186 | Stephan Merz [France] ; Hernán Vanzetto [France] | Encoding TLA+ set theory into many-sorted first-order logic |
000296 | David Déharbe [Brésil] ; Stephan Merz [France] | Software Component Design with the B Method — A Formalization in Isabelle/HOL |
000702 | Carlos Areces [Argentine] ; Pascal Fontaine [France] ; Stephan Merz [France] | Modal Satisfiability via SMT Solving |
000829 | Gerald Lüttgen [Allemagne] ; Stephan Merz [France] | Editorial: Special Issue of Automated Verification of Critical Systems |
000831 | Gerald Lüttgen [Allemagne] ; Stephan Merz [France] | Science of Computer Programming Special Issue: Automated Verification of Critical Systems |
000864 | Jingshu Chen [France] ; Marie Duflot [France] ; Stephan Merz [France] | Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations |
000893 | Stephan Merz [France] ; Jun Pang [Luxembourg (pays)] | Formal Methods and Software Engineering – 16th International Conference on Formal Engineering Methods (ICFEM 2014) |
000A13 | Damien Doligez [France] ; Jael Kriener [France] ; Leslie Lamport [États-Unis] ; Tomer Libal [France] ; Stephan Merz [France] | Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics |
000A24 | Damien Doligez [France] ; Jael Kriener [France] ; Leslie Lamport [États-Unis] ; Tomer Libal [France] ; Stephan Merz [France] | Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics |
000D21 | Stephan Merz [France] ; Hernán Vanzetto [France] | Refinement Types for TLA+ |
001134 | Etienne Mabille [France] ; Marc Boyer [France] ; Loic Féjoz [France] ; Stephan Merz [France] | Certifying Network Calculus in a Proof Assistant |
001201 | Bernadette Charron-Bost [France] ; Stephan Merz [France] ; Andrey Rybalchenko [Allemagne] ; Josef Widder [Autriche] | Formal Verification of Distributed Algorithms |
001464 | Etienne Mabille [France] ; Marc Boyer [France] ; Loïc Fejoz [France] ; Stephan Merz [France] | Towards Certifying Network Calculus |
001975 | Stephan Merz [France] ; Hernán Vanzetto [France] | Harnessing SMT Solvers for TLA+ Proofs |
001982 | Denis Cousineau [France] ; Damien Doligez [France] ; Leslie Lamport [France] ; Stephan Merz [France] ; Daniel Ricketts [États-Unis] ; Hernán Vanzetto [France] | TLA+ Proofs |
001987 | Tianxiang Lu [France] ; Stephan Merz [France] ; Christoph Weidenbach [France] | Formal Verification Of Pastry Using TLA+ |
001A46 | Henri Debrat [France] ; Stephan Merz [France] | Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model |
001A50 | Denis Cousineau [France] ; Damien Doligez [France] ; Leslie Lamport [France] ; Stephan Merz [France] ; Daniel Ricketts [États-Unis] ; Hernán Vanzetto [France] | TLA+ Proofs |
001A54 | Pascal Fontaine [France] ; Stephan Merz [France] ; Christoph Weidenbach [Allemagne] | Combination of disjoint theories: beyond decidability |
001B58 | Stephan Merz [France] | Stuttering Equivalence |
001C21 | Stephan Merz [France] ; Hernán Vanzetto [France] | Automatic Verification Of TLA+ Proof Obligations With SMT Solvers |
002197 | Stephan Merz [France] ; Hernán Vanzetto [France] | Towards certification of TLA+ proof obligations with SMT solvers |
002202 | Pascal Fontaine [France] ; Stephan Merz [France] ; Bruno Woltzenlogel Paleo [France] | Compression of Propositional Resolution Proofs via Partial Regularization |
002203 | David Déharbe [Brésil] ; Pascal Fontaine [France] ; Stephan Merz [France] ; Bruno Woltzenlogel Paleo [France] | Exploiting Symmetry in SMT Problems |
002318 | Stephan Merz [France] ; Martin Quinson [France] ; Cristian Rosa [France] | SimGrid MC: Verification Support for a Multi-API Simulation Platform |
002327 | Stephan Merz [France] ; Tianxiang Lu [Allemagne] ; Christoph Weidenbach [Allemagne] | Towards Verification of the Pastry Protocol using TLA+ |
002618 | Tianxiang Lu [Allemagne, France] ; Stephan Merz [France] ; Christoph Weidenbach [Allemagne] | Towards Verification of the Pastry Protocol Using TLA + |
002696 | Bernadette Charron-Bost [France] ; Henri Debrat [France] ; Stephan Merz [France] | Formal Verification of Consensus Algorithms Tolerating Malicious Faults |
002791 | Sabina Akhtar [France] ; Stephan Merz [France] ; Martin Quinson [France] | A High-Level Language for Modeling Algorithms and Their Properties |
002968 | Sabina Akhtar [France] ; Stephan Merz [France] ; Martin Quinson [France] | A High-Level Language for Modeling Algorithms and their Properties |
002A46 | Dominique Méry [France] ; Stephan Merz [France] | Integrated Formal Methods |
002A70 | Cristian Rosa [France] ; Stephan Merz [France] ; Martin Quinson [France] | A Simple Model of Communication APIs - Application to Dynamic Partial-order Reduction |
002A86 | Kaustuv Chaudhuri [France] ; Damien Doligez [France] ; Leslie Lamport [France] ; Stephan Merz [France] | The TLA+ Proof System: Building a Heterogeneous Verification Platform |
002B00 | Tianxiang Lu [Allemagne] ; Stephan Merz [France] ; Christoph Weidenbach [Allemagne] | Model Checking the Pastry Routing Protocol |
002B50 | Hehua Zhang [République populaire de Chine] ; Stephan Merz [France] ; Ming Gu [République populaire de Chine] | Specifying and Verifying PLC systems with TLA+: a case study |
002B72 | Kaustuv Chaudhuri [France] ; Damien Doligez [France] ; Leslie Lamport [États-Unis] ; Stephan Merz [France] | Verifying Safety Properties With the TLA+ Proof System |
002B78 | Pascal Fontaine [France] ; Stephan Merz [France] ; Bruno Woltzenlogel Paleo [France] | Exploring and Exploiting Algebraic and Graphical Properties of Resolution |
002D94 | Henri Debrat [France] ; Bernadette Charron-Bost [France] ; Stephan Merz [France] | Formal Verification of Consensus Algorithms in a Proof Assistant |
002D99 | Sabina Akhtar [France] ; Stephan Merz [France] ; Martin Quinson [France] | Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms |
003437 | Alexander Schimpf ; Stephan Merz [France] ; Jan-Georg Smaus | Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL |
003439 | Francisco L Pez Fraguas [Espagne] ; Stephan Merz [France] ; Juan Rodríguez Hortalá [Espagne] | A Formalization of the Semantics of Functional-Logic Programming in Isabelle |
003462 | David Déharbe [Brésil] ; Pascal Fontaine [France] ; Anamaria Martins Moreira [Brésil] ; Stephan Merz [France] ; Anderson Santana De Oliveira | Automating model-based software engineering |
003523 | Cristian Rosa [France] ; Martin Quinson [France] ; Stephan Merz [France] | Model-checking Distributed Applications with GRAS |
003773 | Bernadette Charron-Bost [France] ; Stephan Merz [France] | Formal Verification of a Consensus Algorithm in the Heard-Of Model |
003A25 | Mouna Chaouch-Saad [Tunisie] ; Bernadette Charron-Bost [France] ; Stephan Merz [France] | A Reduction Theorem for the Verification of Round-Based Distributed Algorithms |
003C62 | Cristian Rosa [France] ; Martin Quinson [France] ; Stephan Merz [France] | Model-checking Distributed Applications with GRAS |
003F16 | Loïc Fejoz [France] ; Stephan Merz [France] | Towards automatic proofs of lock-free algorithms |
004513 | Stephan Merz [France] | The Specification Language TLA+ |
004519 | Fred Kröger [Allemagne] ; Stephan Merz [France] | Temporal Logic and State Systems |
004551 | Stephan Merz [France] ; Nicolas Navet [France] | Modeling and Verification of Real-Time Systems - Formalisms and Software Tools |
004555 | Serge Autexier [Allemagne] ; Heiko Mantel [Allemagne] ; Stephan Merz [France] ; Tobias Nipkow [Allemagne] | Journal of Automated Reasoning Special Issue: Formal Modeling and Verification of Critical Systems |
004602 | Stephan Merz [France] | An introduction to model checking |
004615 | Kaustuv Chaudhuri [France] ; Damien Doligez [France] ; Leslie Lamport [France] ; Stephan Merz [France] | A TLA+ Proof System |
004840 | Clément Hurlin ; Amine Chaib ; Pascal Fontaine [France] ; Stephan Merz [France] ; Tjark Weber | Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions |
004872 | Loïc Fejoz [France] ; Stephan Merz [France] | Dérivation d'algorithmes sans verrou à partir d'une spécification atomique |
004C00 | Eun-Young Kang [France] ; Stephan Merz [France] | Predicate diagrams for the verification of real-time systems |
004E32 | Dominique Méry [France] ; Stephan Merz [France] | Specification and Refinement of Access Control |
004E44 | Stephan Merz [France] ; Tobias Nipkow [Allemagne] | Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006) |
005165 | Houda Fekih [France] ; Leila Jemni Ben Ayed [Tunisie] ; Stephan Merz [France] | Transformation of B Specifications into UML Class Diagrams and State Machines |
005193 | Dominique Méry [France] ; Stephan Merz [France] | Event Systems and Access Control |
005484 | Pascal Fontaine [France] ; Jean-Yves Marion [France] ; Stephan Merz [France] ; Leonor Prensa Nieto [France] ; Alwen Tiu [France] | Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants |
005589 | Alexander Knapp [Allemagne] ; Stephan Merz [France] ; Martin Wirsing [Allemagne] ; Julia Zappe [Allemagne, France] | Specification and refinement of mobile systems in MTLA and mobile UML |
005632 | Stephan Merz [France] | Model checking : éléments de base |
005915 | Eunyoung Kang [France] ; Stephan Merz [France] | Predicate Diagrams for the Verification of Real-Time Systems |
005A62 | Moritz Hammer [Allemagne] ; Alexander Knapp [Allemagne] ; Stephan Merz [France] | Truly On-The-Fly LTL Model Checking |
005A67 | Loïc Fejoz [France] ; Dominique Méry [France] ; Stephan Merz [France] | DIXIT: a Graphical Toolkit for Predicate Abstractions |
005F61 | Loïc Fejoz ; Dominique Méry [France] ; Stephan Merz | DIXIT : a Graphical Toolkit for Predicate Abstractions |
006165 | Moritz Hammer [Allemagne] ; Alexander Knapp [Allemagne] ; Stephan Merz [France] | Truly On-the-Fly LTL Model Checking |
006B43 | Alexander Knapp [Allemagne] ; Stephan Merz [France] ; Martin Wirsing [Allemagne] | Refining Mobile UML State Machines |
006D28 | Alexander Knapp ; Stephan Merz [France] ; Martin Wirsing | Refining Mobile UML State Machines |
006D55 | Houda Fekih [France] ; Leila Jemni ; Stephan Merz [France] | Transformation des spécifications B en des diagrammes UML |
006E74 | Stephan Merz [France] | TLA+ Case Study: A Resource Allocator |
007B09 | Stephan Merz [France] ; Martin Wirsing [Allemagne] ; Júlia Zappe [Allemagne] | A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems |
007B53 | Stephan Merz [France] | On the logic of TLA+ |
007D33 | Houda Fekih [Tunisie] ; Stephan Merz [France] | Translating B machines into UML diagrams |
007D40 | Mohamed El Habib ; Claude Kirchner [France] ; Hélène Kirchner [France] ; Jean-Yves Marion [France] ; Stephan Merz [France] | The QSL platform at LORIA |
007D78 | Stephan Merz [France] | On the Logic of TLA+ |
007E29 | Stephan Merz [France] ; Ali Sezgin | Emptiness of Linear Weak Alternating Automata |
007E92 | Stephan Merz [France] ; Martin Wirsing ; Julia Zappe | A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems |
008F02 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Formal Analysis of a Self-Stabilizing Algorithm - Using Predicate Diagrams |
009652 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Formal Analysis of a Self-Stabilizing Algorithm - Using Predicate Diagrams |
009B66 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Predicate diagrams |
009C29 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Verifying Reactive Systems Using Predicate Diagrams |
009C67 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Diagrams Refinement for the Design of Reactive Systems |
009C87 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Predicate diagrams for the verification of reactive systems |
009F87 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz [Allemagne] | Predicate diagrams for the verification of reactive systems |
00A007 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Predicate diagrams |
00A112 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Verifying Reactive Systems Using Predicate Diagrams |
00A161 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Predicate diagrams for the verification of reactive systems |
00A235 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Diagrams Refinement for the Design of Reactive Systems |
00A334 | Yassine Mokhtari [France] ; Stephan Merz | Animating TLA Specifications |
00AA41 | Yassine Mokhtari [France] ; Stephan Merz [Allemagne] | Animating TLA Specifications |
This area was generated with Dilib version V0.6.33. |